es:ES, i:Id, P:({e:E| loc(e) = i} {e2:E| loc(e2) = i} ).
e1@i. e2e1.(e:E. (e1 <loc e)  e loc e2   P(e,e2))  P(e1,e2)
 e1@i. e2<e1. P(e1,e2)
 (e, e':E. (loc(e) = i)  (loc(e') = i)  P(e,e')) 

latex

Definitions	t  T, P  Q, x:A. B(x), loc(e), Id, E, b, False, A, , x(s1,s2), x. t(x), e<e'. P(e), e@i. P(e), P & Q, (e <loc e'), ES, t.1, P  Q, e loc e' , e'e.P(e'), Dec(P), P  Q
Lemmas	not functionality wrt iff, es-le-not-locl, not wf, decidable es-locl, decidable es-le, event system wf, alle-ge wf, es-locl wf, es-le wf, es-le-loc, alle-at wf, alle-lt wf, subtype rel self, es-loc-pred, es-E wf, Id wf, es-loc wf, es-interval-induction